Nuprl Lemma : frame-p-realizable
11,40
postcript
pdf
i
,
x
:Id,
T
:Type,
L
:(Knd List). normal-type{i:l}(
T
)
es-real{i:l}(
es
.frame-p(
es
;
i
;
T
;
x
;
L
))
latex
Definitions
x
.
t
(
x
)
,
prop{i:l}
,
t
T
,
x
:
A
.
B
(
x
)
,
es-real{i:l}(
es
.
P
(
es
))
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
(
s
)
Lemmas
Id
wf
,
Knd
wf
,
normal-type
wf
,
event
system
wf
,
frame-p
wf
,
R-realizes
wf
,
R-frame-rule
,
Rframe
wf
origin
i,x:Id, T:Type, L:(Knd List). normal-type{i:l}(T) 
es-real{i:l}(es.frame-p(es; i; T; x; L)) i,x:Id, T:Type, L:(Knd List). normal-type{i:l}(T) es-real{i:l}(es.frame-p(es; i; T; x; L)) 
x. t(x)
T
x:A. B(x) Qx:A. B(x)